<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>LaTeX-succeed</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

\AgdaHide{
</a><a id="74" class="Markup">\begin{code}</a>
<a id="87" class="Keyword">module</a> <a id="94" href="LaTeX-succeed.html" class="Module">LaTeX-succeed</a> <a id="108" class="Keyword">where</a>
<a id="114" class="Markup">\end{code}</a><a id="124" class="Background">
}

</a><a id="128" class="Markup">\begin{code}</a>
<a id="141" class="Keyword">data</a> <a id="Bool"></a><a id="146" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="151" class="Symbol">:</a> <a id="153" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="157" class="Keyword">where</a>
  <a id="Bool.true"></a><a id="165" href="LaTeX-succeed.html#165" class="InductiveConstructor">true</a>   <a id="172" class="Symbol">:</a> <a id="174" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
  <a id="Bool.false"></a><a id="181" href="LaTeX-succeed.html#181" class="InductiveConstructor">false</a>  <a id="188" class="Symbol">:</a> <a id="190" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>

<a id="if_then_else_"></a><a id="196" href="LaTeX-succeed.html#196" class="Function Operator">if_then_else_</a> <a id="210" class="Symbol">:</a> <a id="212" class="Symbol">{</a><a id="213" href="LaTeX-succeed.html#213" class="Bound">A</a> <a id="215" class="Symbol">:</a> <a id="217" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="220" class="Symbol">}</a> <a id="222" class="Symbol">→</a> <a id="224" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="229" class="Symbol">→</a> <a id="231" href="LaTeX-succeed.html#213" class="Bound">A</a> <a id="233" class="Symbol">→</a> <a id="235" href="LaTeX-succeed.html#213" class="Bound">A</a> <a id="237" class="Symbol">→</a> <a id="239" href="LaTeX-succeed.html#213" class="Bound">A</a>
<a id="241" href="LaTeX-succeed.html#196" class="Function Operator">if</a> <a id="244" href="LaTeX-succeed.html#165" class="InductiveConstructor">true</a>   <a id="251" href="LaTeX-succeed.html#196" class="Function Operator">then</a> <a id="256" href="LaTeX-succeed.html#256" class="Bound">t</a> <a id="258" href="LaTeX-succeed.html#196" class="Function Operator">else</a> <a id="263" href="LaTeX-succeed.html#263" class="Bound">f</a> <a id="265" class="Symbol">=</a> <a id="267" href="LaTeX-succeed.html#256" class="Bound">t</a>
<a id="269" href="LaTeX-succeed.html#196" class="Function Operator">if</a> <a id="272" href="LaTeX-succeed.html#181" class="InductiveConstructor">false</a>  <a id="279" href="LaTeX-succeed.html#196" class="Function Operator">then</a> <a id="284" href="LaTeX-succeed.html#284" class="Bound">t</a> <a id="286" href="LaTeX-succeed.html#196" class="Function Operator">else</a> <a id="291" href="LaTeX-succeed.html#291" class="Bound">f</a> <a id="293" class="Symbol">=</a> <a id="295" href="LaTeX-succeed.html#291" class="Bound">f</a>

<a id="298" class="Keyword">data</a> <a id="ℕ"></a><a id="303" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="305" class="Symbol">:</a> <a id="307" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="311" class="Keyword">where</a>
  <a id="ℕ.zero"></a><a id="319" href="LaTeX-succeed.html#319" class="InductiveConstructor">zero</a>  <a id="325" class="Symbol">:</a> <a id="327" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>
  <a id="ℕ.suc"></a><a id="331" href="LaTeX-succeed.html#331" class="InductiveConstructor">suc</a>   <a id="337" class="Symbol">:</a> <a id="339" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="341" class="Symbol">→</a> <a id="343" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>

<a id="_+_"></a><a id="346" href="LaTeX-succeed.html#346" class="Function Operator">_+_</a> <a id="350" class="Symbol">:</a> <a id="352" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="354" class="Symbol">→</a> <a id="356" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="358" class="Symbol">→</a> <a id="360" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>
<a id="362" href="LaTeX-succeed.html#319" class="InductiveConstructor">zero</a>             <a id="379" href="LaTeX-succeed.html#346" class="Function Operator">+</a> <a id="381" href="LaTeX-succeed.html#381" class="Bound">n</a> <a id="383" class="Symbol">=</a> <a id="385" href="LaTeX-succeed.html#381" class="Bound">n</a>
<a id="387" href="LaTeX-succeed.html#331" class="InductiveConstructor">suc</a> <a id="391" href="LaTeX-succeed.html#391" class="Bound">m</a> <a id="393" class="Comment">{- ugh -}</a>  <a id="404" href="LaTeX-succeed.html#346" class="Function Operator">+</a> <a id="406" href="LaTeX-succeed.html#406" class="Bound">n</a> <a id="408" class="Symbol">=</a> <a id="410" href="LaTeX-succeed.html#331" class="InductiveConstructor">suc</a> <a id="414" class="Symbol">(</a><a id="415" href="LaTeX-succeed.html#391" class="Bound">m</a> <a id="417" href="LaTeX-succeed.html#346" class="Function Operator">+</a> <a id="419" href="LaTeX-succeed.html#406" class="Bound">n</a><a id="420" class="Symbol">)</a>

<a id="423" class="Symbol">{-#</a> <a id="427" class="Keyword">BUILTIN</a> <a id="435" class="Keyword">NATURAL</a> <a id="443" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="445" class="Symbol">#-}</a>

<a id="alignment"></a><a id="450" href="LaTeX-succeed.html#450" class="Function">alignment</a> <a id="460" class="Symbol">:</a> <a id="462" class="Symbol">(</a><a id="463" href="LaTeX-succeed.html#463" class="Bound">m</a> <a id="465" href="LaTeX-succeed.html#465" class="Bound">n</a> <a id="467" href="LaTeX-succeed.html#467" class="Bound">o</a> <a id="469" href="LaTeX-succeed.html#469" class="Bound">p</a> <a id="471" class="Symbol">:</a> <a id="473" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a><a id="474" class="Symbol">)</a> <a id="476" class="Symbol">→</a> <a id="478" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>
<a id="480" href="LaTeX-succeed.html#450" class="Function">alignment</a>  <a id="491" class="Number">0</a>  <a id="494" class="Number">1</a>     <a id="500" class="Number">2</a>  <a id="503" class="Number">3</a>     <a id="509" class="Symbol">=</a>  <a id="512" class="Number">4</a>
<a id="514" href="LaTeX-succeed.html#450" class="Function">alignment</a>     <a id="528" class="Number">1</a>  <a id="531" class="Number">2</a>  <a id="534" class="Number">3</a>  <a id="537" class="Number">4</a>  <a id="540" class="Symbol">=</a>  <a id="543" class="Number">5</a>
<a id="545" href="LaTeX-succeed.html#450" class="Function">alignment</a>        <a id="562" class="Number">2</a>  <a id="565" class="Number">3</a>  <a id="568" class="Number">4</a>  <a id="571" class="Number">5</a>     <a id="577" class="Symbol">=</a> <a id="579" class="Number">6</a>
<a id="581" href="LaTeX-succeed.html#450" class="CatchallClause Function">alignment</a><a id="590" class="CatchallClause">           </a><a id="601" class="CatchallClause Symbol">_</a><a id="602" class="CatchallClause">  </a><a id="604" class="CatchallClause Symbol">_</a><a id="605" class="CatchallClause">  </a><a id="607" class="CatchallClause Symbol">_</a><a id="608" class="CatchallClause">  </a><a id="610" class="CatchallClause Symbol">_</a>  <a id="613" class="Symbol">=</a> <a id="615" class="Number">0</a>
<a id="617" class="Markup">\end{code}</a><a id="627" class="Background">

</a><a id="629" class="Markup">\begin{code}</a>
<a id="642" class="Keyword">data</a> <a id="⊥"></a><a id="647" href="LaTeX-succeed.html#647" class="Datatype">⊥</a> <a id="649" class="Symbol">:</a> <a id="651" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="655" class="Keyword">where</a>

<a id="662" class="Keyword">record</a> <a id="R"></a><a id="669" href="LaTeX-succeed.html#669" class="Record">R</a> <a id="671" class="Symbol">:</a> <a id="673" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="678" class="Keyword">where</a>
  <a id="686" class="Keyword">field</a>
    <a id="R.f"></a><a id="696" href="LaTeX-succeed.html#696" class="Field">f</a>  <a id="699" class="Symbol">:</a> <a id="701" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    <a id="R.g"></a><a id="709" href="LaTeX-succeed.html#709" class="Field">g</a>  <a id="712" class="Symbol">:</a> <a id="714" href="Agda.Primitive.html#311" class="Primitive">Set</a>

<a id="719" class="Keyword">record</a> <a id="R′"></a><a id="726" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="729" class="Symbol">(</a><a id="730" href="LaTeX-succeed.html#730" class="Bound">A</a> <a id="732" href="LaTeX-succeed.html#732" class="Bound">B</a> <a id="734" class="Symbol">:</a> <a id="736" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="739" class="Symbol">)</a> <a id="741" class="Symbol">:</a> <a id="743" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="748" class="Keyword">where</a>
  <a id="756" class="Keyword">field</a>
    <a id="R′.h"></a><a id="766" href="LaTeX-succeed.html#766" class="Field">h</a>  <a id="769" class="Symbol">:</a> <a id="771" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    <a id="R′.j"></a><a id="779" href="LaTeX-succeed.html#779" class="Field">j</a>  <a id="782" class="Symbol">:</a> <a id="784" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    <a id="R′.r"></a><a id="792" href="LaTeX-succeed.html#792" class="Field">r</a>  <a id="795" class="Symbol">:</a> <a id="797" href="LaTeX-succeed.html#669" class="Record">R</a>
<a id="799" class="Markup">\end{code}</a><a id="809" class="Background">

</a><a id="811" class="Markup">\begin{code}</a>
<a id="824" class="Keyword">module</a> <a id="M"></a><a id="831" href="LaTeX-succeed.html#831" class="Module">M</a> <a id="833" class="Keyword">where</a>
  <a id="M.r′"></a><a id="841" href="LaTeX-succeed.html#841" class="Function">r′</a> <a id="844" class="Symbol">:</a> <a id="846" class="Symbol">∀</a> <a id="848" class="Symbol">{</a><a id="849" href="LaTeX-succeed.html#849" class="Bound">A</a> <a id="851" href="LaTeX-succeed.html#851" class="Bound">B</a> <a id="853" class="Symbol">:</a> <a id="855" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="858" class="Symbol">}</a> <a id="860" class="Symbol">→</a> <a id="862" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="865" href="LaTeX-succeed.html#849" class="Bound">A</a> <a id="867" href="LaTeX-succeed.html#851" class="Bound">B</a>
  <a id="871" href="LaTeX-succeed.html#841" class="Function">r′</a> <a id="874" class="Symbol">=</a> <a id="876" class="Keyword">record</a>
    <a id="887" class="Symbol">{</a> <a id="889" href="LaTeX-succeed.html#766" class="Field">h</a>  <a id="892" class="Symbol">=</a> <a id="894" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    <a id="900" class="Symbol">;</a> <a id="902" href="LaTeX-succeed.html#779" class="Field">j</a>  <a id="905" class="Symbol">=</a> <a id="907" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    <a id="913" class="Symbol">;</a> <a id="915" href="LaTeX-succeed.html#792" class="Field">r</a> <a id="917" class="Symbol">=</a> <a id="919" class="Keyword">record</a>
        <a id="934" class="Symbol">{</a> <a id="936" href="LaTeX-succeed.html#696" class="Field">f</a>  <a id="939" class="Symbol">=</a> <a id="941" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
        <a id="951" class="Symbol">;</a> <a id="953" href="LaTeX-succeed.html#709" class="Field">g</a>  <a id="956" class="Symbol">=</a> <a id="958" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
        <a id="968" class="Symbol">}</a>
    <a id="974" class="Symbol">}</a>
<a id="976" class="Markup">\end{code}</a><a id="986" class="Background">

Andreas, 2018-04-03: The following two modules test the highlighting of projection patterns.

</a><a id="1082" class="Markup">\begin{code}</a>
<a id="1095" class="Keyword">module</a> <a id="QualifiedProjectionPatterns"></a><a id="1102" href="LaTeX-succeed.html#1102" class="Module">QualifiedProjectionPatterns</a> <a id="1130" class="Keyword">where</a>

  <a id="QualifiedProjectionPatterns.r"></a><a id="1139" href="LaTeX-succeed.html#1139" class="Function">r</a> <a id="1141" class="Symbol">:</a> <a id="1143" href="LaTeX-succeed.html#669" class="Record">R</a>
  <a id="1147" href="LaTeX-succeed.html#1139" class="Function">r</a> <a id="1149" class="Symbol">.</a><a id="1150" href="LaTeX-succeed.html#696" class="Field">R.f</a> <a id="1154" class="Symbol">=</a> <a id="1156" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
  <a id="1163" href="LaTeX-succeed.html#1139" class="Function">r</a> <a id="1165" class="Symbol">.</a><a id="1166" href="LaTeX-succeed.html#709" class="Field">R.g</a> <a id="1170" class="Symbol">=</a> <a id="1172" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>

  <a id="QualifiedProjectionPatterns.r′"></a><a id="1177" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1180" class="Symbol">:</a> <a id="1182" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="1185" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1190" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
  <a id="1194" href="LaTeX-succeed.html#766" class="Field">R′.h</a> <a id="1199" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1202" class="Symbol">=</a> <a id="1204" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
  <a id="1208" href="LaTeX-succeed.html#779" class="Field">R′.j</a> <a id="1213" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1216" class="Symbol">=</a> <a id="1218" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1223" class="Symbol">→</a> <a id="1225" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
  <a id="1232" href="LaTeX-succeed.html#792" class="Field">R′.r</a> <a id="1237" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1240" class="Symbol">=</a> <a id="1242" href="LaTeX-succeed.html#1139" class="Function">r</a>
<a id="1244" class="Markup">\end{code}</a><a id="1254" class="Background">

</a><a id="1256" class="Markup">\begin{code}</a>
<a id="1269" class="Keyword">module</a> <a id="UnqualifiedProjectionPatterns"></a><a id="1276" href="LaTeX-succeed.html#1276" class="Module">UnqualifiedProjectionPatterns</a> <a id="1306" class="Keyword">where</a>
  <a id="1314" class="Keyword">open</a> <a id="1319" href="LaTeX-succeed.html#669" class="Module">R</a><a id="1320" class="Symbol">;</a> <a id="1322" class="Keyword">open</a> <a id="1327" href="LaTeX-succeed.html#726" class="Module">R′</a>

  <a id="UnqualifiedProjectionPatterns.r₀"></a><a id="1333" href="LaTeX-succeed.html#1333" class="Function">r₀</a> <a id="1336" class="Symbol">:</a> <a id="1338" href="LaTeX-succeed.html#669" class="Record">R</a>
  <a id="1342" href="LaTeX-succeed.html#1333" class="Function">r₀</a> <a id="1345" class="Symbol">.</a><a id="1346" href="LaTeX-succeed.html#696" class="Field">f</a> <a id="1348" class="Symbol">=</a> <a id="1350" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
  <a id="1357" href="LaTeX-succeed.html#1333" class="Function">r₀</a> <a id="1360" class="Symbol">.</a><a id="1361" href="LaTeX-succeed.html#709" class="Field">g</a> <a id="1363" class="Symbol">=</a> <a id="1365" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>

  <a id="UnqualifiedProjectionPatterns.r′"></a><a id="1370" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1373" class="Symbol">:</a> <a id="1375" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="1378" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1383" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
  <a id="1387" href="LaTeX-succeed.html#766" class="Field">h</a> <a id="1389" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1392" class="Symbol">=</a> <a id="1394" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
  <a id="1398" href="LaTeX-succeed.html#779" class="Field">j</a> <a id="1400" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1403" class="Symbol">=</a> <a id="1405" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1410" class="Symbol">→</a> <a id="1412" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
  <a id="1419" href="LaTeX-succeed.html#792" class="Field">r</a> <a id="1421" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1424" class="Symbol">=</a> <a id="1426" href="LaTeX-succeed.html#1333" class="Function">r₀</a>
<a id="1429" class="Markup">\end{code}</a><a id="1439" class="Background">

\end{document}
</a></pre></body></html>